ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). (eclor?(x))  (eclor-b(x)  ecl(ds;da)) 

latex

Definitions	x. t(x), if b then t else f fi , tt, ff, eclor-b(x), t  T, eclor?(x), b, P  Q, ecl(ds;da), x:A. B(x), x(s), False, eclcatch(a;l), eclthrow(a;n), a.n, [a]*, eclor(a;b), ecland(a;b), eclseq(a;b), , eclbase(k;test)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, eclor? wf, assert wf, true wf, false wf